↳ ITRS

  ↳ ITRStoIDPProof

z

eval_1(x, y, z) → Cond_eval_1(&&(&&(>@z(y, x), >@z(z, y)), >@z(y, 0@z)), x, y, z)
Cond_eval_11(TRUE, x, y, z) → eval_1(x, y, -@z(x, y))
Cond_eval_1(TRUE, x, y, z) → eval_1(+@z(x, y), y, z)
Cond_eval_0(TRUE, x, y, z) → eval_1(x, y, z)
eval_0(x, y, z) → Cond_eval_0(>@z(y, 0@z), x, y, z)
eval_1(x, y, z) → Cond_eval_11(&&(&&(>@z(y, x), >@z(z, y)), >@z(y, 0@z)), x, y, z)

eval_1(x0, x1, x2)
Cond_eval_11(TRUE, x0, x1, x2)
Cond_eval_1(TRUE, x0, x1, x2)
Cond_eval_0(TRUE, x0, x1, x2)
eval_0(x0, x1, x2)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

z

eval_1(x, y, z) → Cond_eval_1(&&(&&(>@z(y, x), >@z(z, y)), >@z(y, 0@z)), x, y, z)
Cond_eval_11(TRUE, x, y, z) → eval_1(x, y, -@z(x, y))
Cond_eval_1(TRUE, x, y, z) → eval_1(+@z(x, y), y, z)
Cond_eval_0(TRUE, x, y, z) → eval_1(x, y, z)
eval_0(x, y, z) → Cond_eval_0(>@z(y, 0@z), x, y, z)
eval_1(x, y, z) → Cond_eval_11(&&(&&(>@z(y, x), >@z(z, y)), >@z(y, 0@z)), x, y, z)

(0) -> (2), if ((y[0] →^* y[2])∧(z[0] →^* z[2])∧(+@z(x[0], y[0]) →^* x[2]))

(0) -> (3), if ((y[0] →^* y[3])∧(z[0] →^* z[3])∧(+@z(x[0], y[0]) →^* x[3]))

(1) -> (2), if ((y[1] →^* y[2])∧(-@z(x[1], y[1]) →^* z[2])∧(x[1] →^* x[2]))

(1) -> (3), if ((y[1] →^* y[3])∧(-@z(x[1], y[1]) →^* z[3])∧(x[1] →^* x[3]))

(2) -> (1), if ((z[2] →^* z[1])∧(x[2] →^* x[1])∧(y[2] →^* y[1])∧(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)) →^* TRUE))

(3) -> (0), if ((z[3] →^* z[0])∧(x[3] →^* x[0])∧(y[3] →^* y[0])∧(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)) →^* TRUE))

(4) -> (5), if ((z[4] →^* z[5])∧(x[4] →^* x[5])∧(y[4] →^* y[5])∧(>@z(y[4], 0@z) →^* TRUE))

(5) -> (2), if ((y[5] →^* y[2])∧(z[5] →^* z[2])∧(x[5] →^* x[2]))

(5) -> (3), if ((y[5] →^* y[3])∧(z[5] →^* z[3])∧(x[5] →^* x[3]))

eval_1(x0, x1, x2)
Cond_eval_11(TRUE, x0, x1, x2)
Cond_eval_1(TRUE, x0, x1, x2)
Cond_eval_0(TRUE, x0, x1, x2)
eval_0(x0, x1, x2)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

z

(0) -> (2), if ((y[0] →^* y[2])∧(z[0] →^* z[2])∧(+@z(x[0], y[0]) →^* x[2]))

(0) -> (3), if ((y[0] →^* y[3])∧(z[0] →^* z[3])∧(+@z(x[0], y[0]) →^* x[3]))

(1) -> (2), if ((y[1] →^* y[2])∧(-@z(x[1], y[1]) →^* z[2])∧(x[1] →^* x[2]))

(1) -> (3), if ((y[1] →^* y[3])∧(-@z(x[1], y[1]) →^* z[3])∧(x[1] →^* x[3]))

(2) -> (1), if ((z[2] →^* z[1])∧(x[2] →^* x[1])∧(y[2] →^* y[1])∧(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)) →^* TRUE))

(3) -> (0), if ((z[3] →^* z[0])∧(x[3] →^* x[0])∧(y[3] →^* y[0])∧(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)) →^* TRUE))

(4) -> (5), if ((z[4] →^* z[5])∧(x[4] →^* x[5])∧(y[4] →^* y[5])∧(>@z(y[4], 0@z) →^* TRUE))

(5) -> (2), if ((y[5] →^* y[2])∧(z[5] →^* z[2])∧(x[5] →^* x[2]))

(5) -> (3), if ((y[5] →^* y[3])∧(z[5] →^* z[3])∧(x[5] →^* x[3]))

eval_1(x0, x1, x2)
Cond_eval_11(TRUE, x0, x1, x2)
Cond_eval_1(TRUE, x0, x1, x2)
Cond_eval_0(TRUE, x0, x1, x2)
eval_0(x0, x1, x2)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPNonInfProof

z

(2) -> (1), if ((z[2] →^* z[1])∧(x[2] →^* x[1])∧(y[2] →^* y[1])∧(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)) →^* TRUE))

(3) -> (0), if ((z[3] →^* z[0])∧(x[3] →^* x[0])∧(y[3] →^* y[0])∧(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)) →^* TRUE))

(0) -> (3), if ((y[0] →^* y[3])∧(z[0] →^* z[3])∧(+@z(x[0], y[0]) →^* x[3]))

(0) -> (2), if ((y[0] →^* y[2])∧(z[0] →^* z[2])∧(+@z(x[0], y[0]) →^* x[2]))

(1) -> (3), if ((y[1] →^* y[3])∧(-@z(x[1], y[1]) →^* z[3])∧(x[1] →^* x[3]))

(1) -> (2), if ((y[1] →^* y[2])∧(-@z(x[1], y[1]) →^* z[2])∧(x[1] →^* x[2]))

eval_1(x0, x1, x2)
Cond_eval_11(TRUE, x0, x1, x2)
Cond_eval_1(TRUE, x0, x1, x2)
Cond_eval_0(TRUE, x0, x1, x2)
eval_0(x0, x1, x2)

• We consider the chain EVAL_1(x[2], y[2], z[2]) → COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2]), COND_EVAL_11(TRUE, x[1], y[1], z[1]) → EVAL_1(x[1], y[1], -@z(x[1], y[1])), EVAL_1(x[3], y[3], z[3]) → COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]) which results in the following constraint:
  

  (1)    (y[2]=y[1]∧-@z(x[1], y[1])=z[3]∧y[1]=y[3]∧x[2]=x[1]∧z[2]=z[1]∧x[1]=x[3]∧&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z))=TRUE ⇒ COND_EVAL_11(TRUE, x[1], y[1], z[1])≥NonInfC∧COND_EVAL_11(TRUE, x[1], y[1], z[1])≥EVAL_1(x[1], y[1], -@z(x[1], y[1]))∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥))

  
  
  We simplified constraint (1) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (2)    (>@z(y[2], 0@z)=TRUE∧>@z(y[2], x[2])=TRUE∧>@z(z[2], y[2])=TRUE ⇒ COND_EVAL_11(TRUE, x[2], y[2], z[2])≥NonInfC∧COND_EVAL_11(TRUE, x[2], y[2], z[2])≥EVAL_1(x[2], y[2], -@z(x[2], y[2]))∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥))

  
  
  We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (3)    (y[2] + -1 ≥ 0∧y[2] + -1 + (-1)x[2] ≥ 0∧-1 + z[2] + (-1)y[2] ≥ 0 ⇒ (U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧-2 + (-1)Bound + z[2] + (-1)x[2] ≥ 0∧-2 + z[2] + y[2] + (-1)x[2] ≥ 0)

  
  
  We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (4)    (y[2] + -1 ≥ 0∧y[2] + -1 + (-1)x[2] ≥ 0∧-1 + z[2] + (-1)y[2] ≥ 0 ⇒ (U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧-2 + (-1)Bound + z[2] + (-1)x[2] ≥ 0∧-2 + z[2] + y[2] + (-1)x[2] ≥ 0)

  
  
  We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (5)    (y[2] + -1 + (-1)x[2] ≥ 0∧-1 + z[2] + (-1)y[2] ≥ 0∧y[2] + -1 ≥ 0 ⇒ -2 + (-1)Bound + z[2] + (-1)x[2] ≥ 0∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧-2 + z[2] + y[2] + (-1)x[2] ≥ 0)

  
  
  We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (6)    (y[2] + -1 + (-1)x[2] ≥ 0∧z[2] ≥ 0∧y[2] + -1 ≥ 0 ⇒ -1 + (-1)Bound + y[2] + z[2] + (-1)x[2] ≥ 0∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧-1 + (2)y[2] + z[2] + (-1)x[2] ≥ 0)

  
  
  We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (7)    (y[2] + (-1)x[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0 ⇒ (-1)Bound + y[2] + z[2] + (-1)x[2] ≥ 0∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧1 + (2)y[2] + z[2] + (-1)x[2] ≥ 0)

  
  
  We simplified constraint (7) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (8)    (y[2] + (-1)x[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0∧x[2] ≥ 0 ⇒ (-1)Bound + y[2] + z[2] + (-1)x[2] ≥ 0∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧1 + (2)y[2] + z[2] + (-1)x[2] ≥ 0)

  
  

  (9)    (y[2] + x[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0∧x[2] ≥ 0 ⇒ (-1)Bound + y[2] + z[2] + x[2] ≥ 0∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧1 + (2)y[2] + z[2] + x[2] ≥ 0)

  
  
  We simplified constraint (8) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (10)    (y[2] ≥ 0∧z[2] ≥ 0∧x[2] + y[2] ≥ 0∧x[2] ≥ 0 ⇒ (-1)Bound + y[2] + z[2] ≥ 0∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧1 + x[2] + (2)y[2] + z[2] ≥ 0)

  
  
  
• We consider the chain EVAL_1(x[2], y[2], z[2]) → COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2]), COND_EVAL_11(TRUE, x[1], y[1], z[1]) → EVAL_1(x[1], y[1], -@z(x[1], y[1])), EVAL_1(x[2], y[2], z[2]) → COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2]) which results in the following constraint:
  

  (11)    (y[2]=y[1]∧x[2]=x[1]∧-@z(x[1], y[1])=z[2]1∧z[2]=z[1]∧x[1]=x[2]1∧y[1]=y[2]1∧&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z))=TRUE ⇒ COND_EVAL_11(TRUE, x[1], y[1], z[1])≥NonInfC∧COND_EVAL_11(TRUE, x[1], y[1], z[1])≥EVAL_1(x[1], y[1], -@z(x[1], y[1]))∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥))

  
  
  We simplified constraint (11) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (12)    (>@z(y[2], 0@z)=TRUE∧>@z(y[2], x[2])=TRUE∧>@z(z[2], y[2])=TRUE ⇒ COND_EVAL_11(TRUE, x[2], y[2], z[2])≥NonInfC∧COND_EVAL_11(TRUE, x[2], y[2], z[2])≥EVAL_1(x[2], y[2], -@z(x[2], y[2]))∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥))

  
  
  We simplified constraint (12) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (13)    (y[2] + -1 ≥ 0∧y[2] + -1 + (-1)x[2] ≥ 0∧-1 + z[2] + (-1)y[2] ≥ 0 ⇒ (U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧-2 + (-1)Bound + z[2] + (-1)x[2] ≥ 0∧-2 + z[2] + y[2] + (-1)x[2] ≥ 0)

  
  
  We simplified constraint (13) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (14)    (y[2] + -1 ≥ 0∧y[2] + -1 + (-1)x[2] ≥ 0∧-1 + z[2] + (-1)y[2] ≥ 0 ⇒ (U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧-2 + (-1)Bound + z[2] + (-1)x[2] ≥ 0∧-2 + z[2] + y[2] + (-1)x[2] ≥ 0)

  
  
  We simplified constraint (14) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (15)    (y[2] + -1 + (-1)x[2] ≥ 0∧-1 + z[2] + (-1)y[2] ≥ 0∧y[2] + -1 ≥ 0 ⇒ -2 + z[2] + y[2] + (-1)x[2] ≥ 0∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧-2 + (-1)Bound + z[2] + (-1)x[2] ≥ 0)

  
  
  We simplified constraint (15) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (16)    (y[2] + -1 + (-1)x[2] ≥ 0∧z[2] ≥ 0∧y[2] + -1 ≥ 0 ⇒ -1 + (2)y[2] + z[2] + (-1)x[2] ≥ 0∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧-1 + (-1)Bound + y[2] + z[2] + (-1)x[2] ≥ 0)

  
  
  We simplified constraint (16) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (17)    (y[2] ≥ 0∧z[2] ≥ 0∧x[2] + y[2] ≥ 0 ⇒ 1 + x[2] + (2)y[2] + z[2] ≥ 0∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧(-1)Bound + y[2] + z[2] ≥ 0)

  
  
  We simplified constraint (17) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (18)    (y[2] ≥ 0∧z[2] ≥ 0∧x[2] + y[2] ≥ 0∧x[2] ≥ 0 ⇒ 1 + x[2] + (2)y[2] + z[2] ≥ 0∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧(-1)Bound + y[2] + z[2] ≥ 0)

  
  

  (19)    (y[2] ≥ 0∧z[2] ≥ 0∧(-1)x[2] + y[2] ≥ 0∧x[2] ≥ 0 ⇒ 1 + (-1)x[2] + (2)y[2] + z[2] ≥ 0∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧(-1)Bound + y[2] + z[2] ≥ 0)

  
  
  We simplified constraint (19) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (20)    (x[2] + y[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0∧x[2] ≥ 0 ⇒ 1 + x[2] + (2)y[2] + z[2] ≥ 0∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧(-1)Bound + x[2] + y[2] + z[2] ≥ 0)

  
  
  

• We consider the chain EVAL_1(x[2], y[2], z[2]) → COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2]) which results in the following constraint:
  

  (21)    (EVAL_1(x[2], y[2], z[2])≥NonInfC∧EVAL_1(x[2], y[2], z[2])≥COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2])∧(U^Increasing(COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2])), ≥))

  
  
  We simplified constraint (21) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (22)    ((U^Increasing(COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2])), ≥)∧0 ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (22) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (23)    ((U^Increasing(COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2])), ≥)∧0 ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (23) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (24)    ((U^Increasing(COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2])), ≥)∧0 ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (24) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (25)    (0 = 0∧0 = 0∧0 = 0∧(U^Increasing(COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2])), ≥)∧0 = 0∧1 ≥ 0∧0 = 0∧0 ≥ 0∧0 = 0)

  
  
  

• We consider the chain EVAL_1(x[3], y[3], z[3]) → COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]) which results in the following constraint:
  

  (26)    (EVAL_1(x[3], y[3], z[3])≥NonInfC∧EVAL_1(x[3], y[3], z[3])≥COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])∧(U^Increasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥))

  
  
  We simplified constraint (26) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (27)    ((U^Increasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (27) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (28)    ((U^Increasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (28) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (29)    (0 ≥ 0∧(U^Increasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (29) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (30)    (0 ≥ 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧(U^Increasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥))

  
  
  

• We consider the chain EVAL_1(x[3], y[3], z[3]) → COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]), COND_EVAL_1(TRUE, x[0], y[0], z[0]) → EVAL_1(+@z(x[0], y[0]), y[0], z[0]), EVAL_1(x[3], y[3], z[3]) → COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]) which results in the following constraint:
  

  (31)    (z[0]=z[3]1∧+@z(x[0], y[0])=x[3]1∧x[3]=x[0]∧y[3]=y[0]∧&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z))=TRUE∧y[0]=y[3]1∧z[3]=z[0] ⇒ COND_EVAL_1(TRUE, x[0], y[0], z[0])≥NonInfC∧COND_EVAL_1(TRUE, x[0], y[0], z[0])≥EVAL_1(+@z(x[0], y[0]), y[0], z[0])∧(U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥))

  
  
  We simplified constraint (31) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (32)    (>@z(y[3], 0@z)=TRUE∧>@z(y[3], x[3])=TRUE∧>@z(z[3], y[3])=TRUE ⇒ COND_EVAL_1(TRUE, x[3], y[3], z[3])≥NonInfC∧COND_EVAL_1(TRUE, x[3], y[3], z[3])≥EVAL_1(+@z(x[3], y[3]), y[3], z[3])∧(U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥))

  
  
  We simplified constraint (32) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (33)    (-1 + y[3] ≥ 0∧-1 + y[3] + (-1)x[3] ≥ 0∧-1 + z[3] + (-1)y[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧0 ≥ 0∧y[3] ≥ 0)

  
  
  We simplified constraint (33) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (34)    (-1 + y[3] ≥ 0∧-1 + y[3] + (-1)x[3] ≥ 0∧-1 + z[3] + (-1)y[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧0 ≥ 0∧y[3] ≥ 0)

  
  
  We simplified constraint (34) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (35)    (-1 + y[3] + (-1)x[3] ≥ 0∧-1 + z[3] + (-1)y[3] ≥ 0∧-1 + y[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧y[3] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (35) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (36)    (-1 + y[3] + (-1)x[3] ≥ 0∧z[3] ≥ 0∧-1 + y[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧y[3] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (36) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (37)    (y[3] ≥ 0∧z[3] ≥ 0∧x[3] + y[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + x[3] + y[3] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (37) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (38)    (y[3] ≥ 0∧z[3] ≥ 0∧x[3] + y[3] ≥ 0∧x[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + x[3] + y[3] ≥ 0∧0 ≥ 0)

  
  

  (39)    (y[3] ≥ 0∧z[3] ≥ 0∧(-1)x[3] + y[3] ≥ 0∧x[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + (-1)x[3] + y[3] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (39) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (40)    (x[3] + y[3] ≥ 0∧z[3] ≥ 0∧y[3] ≥ 0∧x[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + y[3] ≥ 0∧0 ≥ 0)

  
  
  
• We consider the chain EVAL_1(x[3], y[3], z[3]) → COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]), COND_EVAL_1(TRUE, x[0], y[0], z[0]) → EVAL_1(+@z(x[0], y[0]), y[0], z[0]), EVAL_1(x[2], y[2], z[2]) → COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2]) which results in the following constraint:
  

  (41)    (z[0]=z[2]∧y[0]=y[2]∧x[3]=x[0]∧y[3]=y[0]∧&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z))=TRUE∧+@z(x[0], y[0])=x[2]∧z[3]=z[0] ⇒ COND_EVAL_1(TRUE, x[0], y[0], z[0])≥NonInfC∧COND_EVAL_1(TRUE, x[0], y[0], z[0])≥EVAL_1(+@z(x[0], y[0]), y[0], z[0])∧(U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥))

  
  
  We simplified constraint (41) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (42)    (>@z(y[3], 0@z)=TRUE∧>@z(y[3], x[3])=TRUE∧>@z(z[3], y[3])=TRUE ⇒ COND_EVAL_1(TRUE, x[3], y[3], z[3])≥NonInfC∧COND_EVAL_1(TRUE, x[3], y[3], z[3])≥EVAL_1(+@z(x[3], y[3]), y[3], z[3])∧(U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥))

  
  
  We simplified constraint (42) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (43)    (-1 + y[3] ≥ 0∧-1 + y[3] + (-1)x[3] ≥ 0∧-1 + z[3] + (-1)y[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧0 ≥ 0∧y[3] ≥ 0)

  
  
  We simplified constraint (43) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (44)    (-1 + y[3] ≥ 0∧-1 + y[3] + (-1)x[3] ≥ 0∧-1 + z[3] + (-1)y[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧0 ≥ 0∧y[3] ≥ 0)

  
  
  We simplified constraint (44) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (45)    (-1 + y[3] + (-1)x[3] ≥ 0∧-1 + z[3] + (-1)y[3] ≥ 0∧-1 + y[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧y[3] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (45) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (46)    (-1 + y[3] + (-1)x[3] ≥ 0∧z[3] ≥ 0∧-1 + y[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧y[3] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (46) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (47)    (y[3] + (-1)x[3] ≥ 0∧z[3] ≥ 0∧y[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + y[3] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (47) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (48)    (y[3] + (-1)x[3] ≥ 0∧z[3] ≥ 0∧y[3] ≥ 0∧x[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + y[3] ≥ 0∧0 ≥ 0)

  
  

  (49)    (y[3] + x[3] ≥ 0∧z[3] ≥ 0∧y[3] ≥ 0∧x[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + y[3] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (48) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (50)    (y[3] ≥ 0∧z[3] ≥ 0∧x[3] + y[3] ≥ 0∧x[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + x[3] + y[3] ≥ 0∧0 ≥ 0)

  
  
  

• COND_EVAL_11(TRUE, x[1], y[1], z[1]) → EVAL_1(x[1], y[1], -@z(x[1], y[1]))
  
  • (y[2] + x[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0∧x[2] ≥ 0 ⇒ (-1)Bound + y[2] + z[2] + x[2] ≥ 0∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧1 + (2)y[2] + z[2] + x[2] ≥ 0)
    
  • (y[2] ≥ 0∧z[2] ≥ 0∧x[2] + y[2] ≥ 0∧x[2] ≥ 0 ⇒ (-1)Bound + y[2] + z[2] ≥ 0∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧1 + x[2] + (2)y[2] + z[2] ≥ 0)
    
  • (y[2] ≥ 0∧z[2] ≥ 0∧x[2] + y[2] ≥ 0∧x[2] ≥ 0 ⇒ 1 + x[2] + (2)y[2] + z[2] ≥ 0∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧(-1)Bound + y[2] + z[2] ≥ 0)
    
  • (x[2] + y[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0∧x[2] ≥ 0 ⇒ 1 + x[2] + (2)y[2] + z[2] ≥ 0∧(U^Increasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧(-1)Bound + x[2] + y[2] + z[2] ≥ 0)
    
  
  
• EVAL_1(x[2], y[2], z[2]) → COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2])
  
  • (0 = 0∧0 = 0∧0 = 0∧(U^Increasing(COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2])), ≥)∧0 = 0∧1 ≥ 0∧0 = 0∧0 ≥ 0∧0 = 0)
    
  
  
• EVAL_1(x[3], y[3], z[3]) → COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])
  
  • (0 ≥ 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧(U^Increasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥))
    
  
  
• COND_EVAL_1(TRUE, x[0], y[0], z[0]) → EVAL_1(+@z(x[0], y[0]), y[0], z[0])
  
  • (y[3] ≥ 0∧z[3] ≥ 0∧x[3] + y[3] ≥ 0∧x[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + x[3] + y[3] ≥ 0∧0 ≥ 0)
    
  • (x[3] + y[3] ≥ 0∧z[3] ≥ 0∧y[3] ≥ 0∧x[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + y[3] ≥ 0∧0 ≥ 0)
    
  • (y[3] + x[3] ≥ 0∧z[3] ≥ 0∧y[3] ≥ 0∧x[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + y[3] ≥ 0∧0 ≥ 0)
    
  • (y[3] ≥ 0∧z[3] ≥ 0∧x[3] + y[3] ≥ 0∧x[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + x[3] + y[3] ≥ 0∧0 ≥ 0)
    
  
  

POL(-@z(x₁, x₂)) = x₁ + (-1)x₂   
POL(0@z) = 0   
POL(EVAL_1(x₁, x₂, x₃)) = -1 + x₃ + (-1)x₁   
POL(COND_EVAL_1(x₁, x₂, x₃, x₄)) = -1 + x₄ + (-1)x₂   
POL(TRUE) = -1   
POL(&&(x₁, x₂)) = -1   
POL(+@z(x₁, x₂)) = x₁ + x₂   
POL(FALSE) = -1   
POL(undefined) = -1   
POL(>@z(x₁, x₂)) = -1   
POL(COND_EVAL_11(x₁, x₂, x₃, x₄)) = -1 + x₄ + (-1)x₂ + x₁   

COND_EVAL_11(TRUE, x[1], y[1], z[1]) → EVAL_1(x[1], y[1], -@z(x[1], y[1]))

COND_EVAL_11(TRUE, x[1], y[1], z[1]) → EVAL_1(x[1], y[1], -@z(x[1], y[1]))

EVAL_1(x[2], y[2], z[2]) → COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2])
EVAL_1(x[3], y[3], z[3]) → COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])
COND_EVAL_1(TRUE, x[0], y[0], z[0]) → EVAL_1(+@z(x[0], y[0]), y[0], z[0])

&&(FALSE, FALSE)¹ ↔ FALSE¹
-@z¹ ↔
+@z¹ ↔
&&(TRUE, TRUE)¹ ↔ TRUE¹
&&(TRUE, FALSE)¹ ↔ FALSE¹
&&(FALSE, TRUE)¹ ↔ FALSE¹

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPNonInfProof

                ↳ IDP

                  ↳ IDependencyGraphProof

z

(3) -> (0), if ((z[3] →^* z[0])∧(x[3] →^* x[0])∧(y[3] →^* y[0])∧(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)) →^* TRUE))

(0) -> (3), if ((y[0] →^* y[3])∧(z[0] →^* z[3])∧(+@z(x[0], y[0]) →^* x[3]))

(0) -> (2), if ((y[0] →^* y[2])∧(z[0] →^* z[2])∧(+@z(x[0], y[0]) →^* x[2]))

eval_1(x0, x1, x2)
Cond_eval_11(TRUE, x0, x1, x2)
Cond_eval_1(TRUE, x0, x1, x2)
Cond_eval_0(TRUE, x0, x1, x2)
eval_0(x0, x1, x2)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPNonInfProof

                ↳ IDP

                  ↳ IDependencyGraphProof

                    ↳ IDP

                      ↳ IDPNonInfProof

z

(3) -> (0), if ((z[3] →^* z[0])∧(x[3] →^* x[0])∧(y[3] →^* y[0])∧(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)) →^* TRUE))

(0) -> (3), if ((y[0] →^* y[3])∧(z[0] →^* z[3])∧(+@z(x[0], y[0]) →^* x[3]))

eval_1(x0, x1, x2)
Cond_eval_11(TRUE, x0, x1, x2)
Cond_eval_1(TRUE, x0, x1, x2)
Cond_eval_0(TRUE, x0, x1, x2)
eval_0(x0, x1, x2)

• We consider the chain EVAL_1(x[3], y[3], z[3]) → COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]) which results in the following constraint:
  

  (1)    (EVAL_1(x[3], y[3], z[3])≥NonInfC∧EVAL_1(x[3], y[3], z[3])≥COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])∧(U^Increasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥))

  
  
  We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (2)    ((U^Increasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (3)    ((U^Increasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (4)    (0 ≥ 0∧0 ≥ 0∧(U^Increasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥))

  
  
  We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (5)    (0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧(U^Increasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 = 0)

  
  
  

• We consider the chain EVAL_1(x[3], y[3], z[3]) → COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]), COND_EVAL_1(TRUE, x[0], y[0], z[0]) → EVAL_1(+@z(x[0], y[0]), y[0], z[0]), EVAL_1(x[3], y[3], z[3]) → COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]) which results in the following constraint:
  

  (6)    (z[0]=z[3]1∧+@z(x[0], y[0])=x[3]1∧x[3]=x[0]∧y[3]=y[0]∧&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z))=TRUE∧y[0]=y[3]1∧z[3]=z[0] ⇒ COND_EVAL_1(TRUE, x[0], y[0], z[0])≥NonInfC∧COND_EVAL_1(TRUE, x[0], y[0], z[0])≥EVAL_1(+@z(x[0], y[0]), y[0], z[0])∧(U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥))

  
  
  We simplified constraint (6) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (7)    (>@z(y[3], 0@z)=TRUE∧>@z(y[3], x[3])=TRUE∧>@z(z[3], y[3])=TRUE ⇒ COND_EVAL_1(TRUE, x[3], y[3], z[3])≥NonInfC∧COND_EVAL_1(TRUE, x[3], y[3], z[3])≥EVAL_1(+@z(x[3], y[3]), y[3], z[3])∧(U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥))

  
  
  We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (8)    (-1 + y[3] ≥ 0∧-1 + y[3] + (-1)x[3] ≥ 0∧-1 + z[3] + (-1)y[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + (-1)Bound + (2)z[3] + (-1)y[3] + (-1)x[3] ≥ 0∧-1 + y[3] ≥ 0)

  
  
  We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (9)    (-1 + y[3] ≥ 0∧-1 + y[3] + (-1)x[3] ≥ 0∧-1 + z[3] + (-1)y[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + (-1)Bound + (2)z[3] + (-1)y[3] + (-1)x[3] ≥ 0∧-1 + y[3] ≥ 0)

  
  
  We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (10)    (-1 + y[3] ≥ 0∧-1 + y[3] + (-1)x[3] ≥ 0∧-1 + z[3] + (-1)y[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + (-1)Bound + (2)z[3] + (-1)y[3] + (-1)x[3] ≥ 0∧-1 + y[3] ≥ 0)

  
  
  We simplified constraint (10) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (11)    (-1 + y[3] ≥ 0∧-1 + y[3] + (-1)x[3] ≥ 0∧z[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧3 + (-1)Bound + y[3] + (2)z[3] + (-1)x[3] ≥ 0∧-1 + y[3] ≥ 0)

  
  
  We simplified constraint (11) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (12)    (y[3] ≥ 0∧y[3] + (-1)x[3] ≥ 0∧z[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧4 + (-1)Bound + y[3] + (2)z[3] + (-1)x[3] ≥ 0∧y[3] ≥ 0)

  
  
  We simplified constraint (12) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (13)    (y[3] ≥ 0∧y[3] + (-1)x[3] ≥ 0∧z[3] ≥ 0∧x[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧4 + (-1)Bound + y[3] + (2)z[3] + (-1)x[3] ≥ 0∧y[3] ≥ 0)

  
  

  (14)    (y[3] ≥ 0∧y[3] + x[3] ≥ 0∧z[3] ≥ 0∧x[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧4 + (-1)Bound + y[3] + (2)z[3] + x[3] ≥ 0∧y[3] ≥ 0)

  
  
  We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (15)    (x[3] + y[3] ≥ 0∧y[3] ≥ 0∧z[3] ≥ 0∧x[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧4 + (-1)Bound + y[3] + (2)z[3] ≥ 0∧x[3] + y[3] ≥ 0)

  
  
  

• EVAL_1(x[3], y[3], z[3]) → COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])
  
  • (0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧(U^Increasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 = 0)
    
  
  
• COND_EVAL_1(TRUE, x[0], y[0], z[0]) → EVAL_1(+@z(x[0], y[0]), y[0], z[0])
  
  • (y[3] ≥ 0∧y[3] + x[3] ≥ 0∧z[3] ≥ 0∧x[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧4 + (-1)Bound + y[3] + (2)z[3] + x[3] ≥ 0∧y[3] ≥ 0)
    
  • (x[3] + y[3] ≥ 0∧y[3] ≥ 0∧z[3] ≥ 0∧x[3] ≥ 0 ⇒ (U^Increasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧4 + (-1)Bound + y[3] + (2)z[3] ≥ 0∧x[3] + y[3] ≥ 0)
    
  
  

POL(0@z) = 0   
POL(EVAL_1(x₁, x₂, x₃)) = 1 + (2)x₃ + (-1)x₂ + (-1)x₁   
POL(COND_EVAL_1(x₁, x₂, x₃, x₄)) = 1 + (2)x₄ + (-1)x₃ + (-1)x₂   
POL(TRUE) = 0   
POL(&&(x₁, x₂)) = 1   
POL(+@z(x₁, x₂)) = x₁ + x₂   
POL(FALSE) = 0   
POL(undefined) = -1   
POL(>@z(x₁, x₂)) = -1   

COND_EVAL_1(TRUE, x[0], y[0], z[0]) → EVAL_1(+@z(x[0], y[0]), y[0], z[0])

COND_EVAL_1(TRUE, x[0], y[0], z[0]) → EVAL_1(+@z(x[0], y[0]), y[0], z[0])

EVAL_1(x[3], y[3], z[3]) → COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])

&&(FALSE, FALSE)¹ → FALSE¹
+@z¹ ↔
&&(TRUE, TRUE)¹ → TRUE¹
&&(TRUE, FALSE)¹ → FALSE¹
&&(FALSE, TRUE)¹ → FALSE¹

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPNonInfProof

                ↳ IDP

                  ↳ IDependencyGraphProof

                    ↳ IDP

                      ↳ IDPNonInfProof

                        ↳ IDP

                          ↳ IDependencyGraphProof

z

eval_1(x0, x1, x2)
Cond_eval_11(TRUE, x0, x1, x2)
Cond_eval_1(TRUE, x0, x1, x2)
Cond_eval_0(TRUE, x0, x1, x2)
eval_0(x0, x1, x2)